package useless;

import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import sign.FormulaSign;
import useless.Solution;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.Set;

public class test_Algorithm {
    public static void main(String[] args) {
        UnaryFormula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        UnaryFormula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,q,l);//ANY(q,l)

        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p,q);//Exist(p,q)

        UnaryFormula not_p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),true));
        BinaryFormula f4=new BinaryFormula(FormulaSign.EXIST,not_p,q);//Exist(not p,q)

        ArrayList<Proof> conditions=new ArrayList<>();
        Proof p1=new ConclusionProof(f1);
        Proof p2=new ConclusionProof(f2);
        Proof p4=new ConclusionProof(f4);
        conditions.add(p1);
        conditions.add(p2);
        conditions.add(p4);//ANY(q,l),Exist(p,q),Exist(not p,q)

        Solution solution=new Solution();
        ArrayList<Proof> anyList=solution.Separate_ANY(conditions);
        for (Proof any:anyList) {
            System.out.println(any);
        }
        System.out.println("------------");
        ArrayList<Proof> existList=solution.Separate_EXIST(conditions);
        for (Proof exist:existList) {
            System.out.println(exist);
        }
        System.out.println("----------------");
        //上面部分的any，exist分离测试成功

        //下面测试算法(成功)
        Set<Proof> set=solution.fun(anyList,existList,new HashSet<>(existList));
        for (Proof s:set){
            System.out.println(s.getConclusion().toString());
        }



    }
}
